/* TIPI DI STATO */
sig Str { }

one sig dataCorrente{
	value: Int
	}{ value = 2 }

/* DEFINIZIONI DI ENTITA' */

sig Indirizzo {
	via: one Str,
	cap: one Str,
	citta: one Str,
	provincia: one Str,
	nazione: one Str
	}

abstract sig Utente {
	username: one Str,
	password: one Str
	}

sig UtenteRegistrato extends Utente {
	nome: one Str,
	cognome: one Str,
	indirizzo: one Indirizzo,
	email: one Str,
	dataNascita: Int
	} { dataNascita > 0}

sig Impiegato extends Utente {}

sig Volo {
	cittaDiPartenza: one Str,
	destinazione: one Str,
	dataAndata: Int,
	dataRitorno: Int,
	orarioAndata: Int,
	orarioRitorno: Int,
	aeroportoAndata: one Str,
	aeroportoRitorno: one Str,
	posto: Int
	} { 
	posto > 0
	and dataAndata > 0
	and dataRitorno > 0
	and orarioAndata > 0
	and orarioRitorno > 0 }

sig Hotel {
	nomeHotel: one Str,
	indirizzoHotel: one Indirizzo,
	stelle: Int
	} {	
	stelle > 0
	and stelle < 6 }

sig Camera {
	hotel: one Hotel,
	numeroCamera: Int,
	} { 
	numeroCamera > 0 }

sig Alloggio {
	camera: some Camera,
	ospite: some UtenteRegistrato,
	dataArrivo: Int,
	dataPartenza: Int
	}

sig Pacchetto {
	travelID: one Str,
	voloPacchetto: some Volo,
	cameraPacchetto: some Camera,
	creatoDa: one Impiegato
	}

sig Prenotazione {
	reservationID: one Str,
	pacchetto: one Pacchetto,
	alloggio: some Alloggio,
	numeroPartecipanti: Int,
	dataPrenotazione: Int
	} { 
	numeroPartecipanti > 0
	and dataPrenotazione > 0 }

/* FACT */

/* VINCOLI SUI PACCHETTI */

//Due pacchetti non possono avere lo stesso volo
fact pacchettoConStesstoVolo{ 
	all disj p, p': Pacchetto | no v: Volo | v in p.voloPacchetto and v in p'.voloPacchetto
	}

//Due pacchetti non possono avere la stessa camera
fact pacchettoConStessaCamera{
	all disj p, p': Pacchetto | no c: Camera | c in p.cameraPacchetto and c in p'.cameraPacchetto 
	}

//Un indirizzo deve per forza appartenere o a un albergo o a un utente registrato
fact noIndirizzoSenzaProprietari {
	all i: Indirizzo | i in ( UtenteRegistrato.indirizzo + Hotel.indirizzoHotel)
	}

//Ogni hotel deve avere un indirizzo diverso
fact hotelConIndirizziDiversi {
	all disj h, h': Hotel | no i: Indirizzo | i in h.indirizzoHotel and i in h'.indirizzoHotel
	}

//Due utenti non possono avere lo stesso username
fact usernameDiversi {
	no disj u, u': UtenteRegistrato | u.username = u'.username
	}

//Due pacchetti viaggio non possono avere lo stesso TravelID
fact travelIdDiversi {
	no disj p, p': Pacchetto | p.travelID = p'.travelID
	}

//Due prenotazioni non possono avere lo stesso identicativo
fact reservationIdDiversi {
	no disj p, p': Prenotazione | p.reservationID = p'.reservationID
	}

//Due hotel non posso avere lo stesso nome nella stessa città
fact hotelDiversi {
	no disj h, h': Hotel | h.nomeHotel = h'.nomeHotel and h.indirizzoHotel = h'.indirizzoHotel
	}

//Il numero dei voli deve essere uguale al numero dei partecipanti
fact voliUgualeAPartecipanti {
	all p: Prenotazione | p.numeroPartecipanti = #p.pacchetto.voloPacchetto
	}

//Il cliente può alleggiare solo in una delle camere messe a disposizione del pacchetto
fact {
	all pr: Prenotazione | all pa: Pacchetto | pa in pr.pacchetto implies pr.alloggio.camera in pa.cameraPacchetto
	}

//Se non c'è nessuna prenotazione non ci devono essere alloggi assegnati
	fact {
	all a: Alloggio | some p: Prenotazione | a in p.alloggio
	}

//Un alloggio non può avere più prenotazioni
fact {
	all disj p, p': Prenotazione | no a: Alloggio | a in p.alloggio and a in p'.alloggio
	}

/* VINCOLI SULLE DATE */

//Il volo di andata deve venire prima del volo di ritorno
fact voloAndataPrimaDelVoloRitorno {
	all v: Volo | v.dataAndata <= v.dataRitorno
	}

//La data di prenotazione deve essere precedente alla data di andata
fact dataPrenotazionePrecedenteDataAndata {
	all p: Prenotazione | all v: Volo | v in p.pacchetto.voloPacchetto implies p.dataPrenotazione < v.dataAndata 
	}

//La data di nascita deve essere precedente alla data di prenotazione
fact dataNascitaPrecedenteDataPrenotazione {
	all u: UtenteRegistrato | all p: Prenotazione | u in p.alloggio.ospite implies u.dataNascita < p.dataPrenotazione
	}

//Se la data di andata e la data di ritorno è la stessa, l'orario di andata deve venire prima dell'orario di ritorno
fact oraAndataPrimaOraRitorno {
	all v: Volo | v.dataAndata = v.dataRitorno implies v.orarioAndata < v.orarioRitorno
	}

//Data di partenza dell'aereo deve essere uguale alla data di arrivo in albergo
fact dataPartenzaAereoUgualeDataArrivoCamera {
	all pr: Prenotazione | all pa: pr.pacchetto | all a: pr.alloggio | pa.voloPacchetto.dataAndata = a.dataArrivo and pa.voloPacchetto.dataRitorno = a.dataPartenza
	}

/* PREDICATES */

pred inserisciPacchetto ( p0: Pacchetto, id: Str, v: some Volo, c: some Camera, i: Impiegato ) {
	//Precondizione
	all volo: Volo | volo in v implies v.dataAndata > dataCorrente.value
	//Postcondizione
	p0.travelID = id
	p0.voloPacchetto = v
	p0.cameraPacchetto = c
	p0.creatoDa = i
	}

pred inserisciAlloggio ( a0: Alloggio, u: some UtenteRegistrato, c: some Camera, dArrivo, dPartenza: Int ) {
	//Precondizione
	dArrivo > dataCorrente.value 
		and dPartenza > dArrivo
	//Postcondizione
	a0.camera = c
	a0.ospite = u
	a0.dataArrivo = dArrivo
	a0.dataPartenza = dPartenza
	}

//La data in input è la data di arrivo e di partenza dell'alloggio
pred inserisciPrenotazione ( p0: Prenotazione, a0: Alloggio, id: Str, p: Pacchetto, u: some UtenteRegistrato, c: some Camera, v: some Volo, numPartecipanti, dArrivo, dPartenza: Int ) {
	//Precondizione
	dArrivo > dataCorrente.value 
		and dPartenza > dArrivo 
		and c in p.cameraPacchetto 
		and v in p.voloPacchetto
		and #p.voloPacchetto >= numPartecipanti 
		and #p.cameraPacchetto >= #u
	//Postcondizione
	p0.reservationID = id
	p0.pacchetto = p
	p0.numeroPartecipanti = numPartecipanti
	p0.dataPrenotazione = dataCorrente.value
	inserisciAlloggio[ a0, u, c, dArrivo, dPartenza ]
	p0.alloggio = a0
}	

pred show {}

/* ASSERTIONS */

//Ogni pacchetto ha un TravelID unico
assert travelIdUnivoco {
	all disj p, p': Pacchetto, id: Str, v: Volo, c: Camera, i: Impiegato |
		inserisciPacchetto[ p, id,v, c, i ] implies ( p'.travelID != p.travelID ) 
	}

check travelIdUnivoco

//Ogni prenotazione ha un reservationID unico
assert reservationIdUnico {
	all disj pr, pr': Prenotazione, a: Alloggio, id: Str, pa: Pacchetto, u: some Utente, c: some Camera, v: some Volo, numPartecipanti, dArrivo, dPartenza: Int |
		inserisciPrenotazione[ pr, a, id, pa, u, c, v, numPartecipanti, dArrivo, dPartenza ] implies( pr.reservationID != pr'.reservationID )
	}

check reservationIdUnico 

run inserisciPrenotazione for 5
run inserisciPacchetto for 5
run inserisciAlloggio for 5
run show for 5

